/*
 * Alloy Analyzer 4 -- Copyright (c) 2006-2008, Felix Chang
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
 * copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be included in
 * all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
 * THE SOFTWARE.
 */

package edu.ut.ece382c.valloy.ast;

import java.util.ArrayList;
import java.util.List;
import edu.mit.csail.sdg.alloy4.Pos;
import edu.mit.csail.sdg.alloy4.Err;
import edu.mit.csail.sdg.alloy4.ConstList;
import edu.mit.csail.sdg.alloy4.ConstList.TempList;
import edu.mit.csail.sdg.alloy4.JoinableList;


/**
 * Immutable; represents disjoint[] or pred/totalOrder[] or (... and ... and ..) and other similar list of arugments.
 *
 * <p> <b>Invariant:</b>  type!=EMPTY => (all x:args | x.mult==0)
 */

public final class ExprList extends Expr {

    /** This class contains all possible builtin predicates. */
    public static enum Op {
       /** JOIN (set join using bracket notation or fun/pred call)    */ JOIN(""),
       /** DISJOINT (meaning the argument relations are all disjoint) */ DISJOINT("disj"),
       /** TOTALORDER (meaning it's a total order over the arguments) */ TOTALORDER("pred/totalOrder"),
       /** AND (meaning the logical conjunction of all arguments)     */ AND("and"),
       /** OR (meaning the logical disjunction of all arguments)      */ OR("or");
       
       /** The constructor. */
       private Op(String label) {this.label=label;}

       /** The human readable label for this operator. */
       private final String label;

       /** Returns the human readable label for this operator */
       @Override public final String toString() { return label; }
    };

    /** The builtin operator. */
    public final Op op;

    /** The unmodifiable list of arguments. */
    public final ConstList<Expr> args;

    /** Caches the span() result. */
    private Pos span = null;

    //============================================================================================================//

    /** {@inheritDoc} */
    @Override public Pos span() {
        Pos p=span;
        if (p==null) {
            p=pos.merge(closingBracket);
            for(Expr a:args) p=p.merge(a.span());
            span=p;
        }
        return p;
    }

    //============================================================================================================//

    /** {@inheritDoc} */
    @Override public void toString(StringBuilder out, int indent, boolean newline) {
    	for(int i=0; i<indent && newline; i++) { out.append(' '); }
    	
    	//
    	// pred/totalOrder | disjoin expression list
    	//
    	if (op == Op.TOTALORDER || op == Op.DISJOINT || op == Op.JOIN)
    	{
    		String arglist = "";
        	for(Expr a:args) {
        		if (arglist.length() != 0) 
        			arglist += ", ";
        		arglist += a.toString();
        	}
        	out.append(op.toString() + "[" + arglist + "]");
    		return;
    	}
	
    	//
    	// AND/OR expression list
    	//
    	String opstr = "";
    	
    	if (op == Op.OR) 
    		opstr = " " + op.toString() + " ";
    	if (op == Op.AND)
    		opstr = " " + op.toString() + "\n";
    	
    	newline = false;
    	
    	for (int i = 0; i < args.size(); ++i){
    		if (i != 0) out.append(opstr);
    		Expr e = args.get(i);
    		ExprUnary.Op.NOOP.make(e.pos(), e).toString(out, indent, newline);
    		newline = (op == Op.AND);
    	}
    }

    //============================================================================================================//

    /** Constructs an ExprList node. */
    private ExprList (Pos pos, Pos closingBracket, Op op, boolean ambiguous, ConstList<Expr> args, long weight, JoinableList<Err> errs) {
        super(pos, closingBracket, ambiguous, Type.FORMULA, 0, weight, errs);
        this.op = op;
        this.args = args;
    }

    //============================================================================================================//

    /** Add expr to list, in a way that flattens the conjunctions as much as possible (for better unsat core). */
    private static void addAND(TempList<Expr> list, Expr expr) {
        Expr x = expr;
        if (x instanceof ExprBinary && ((ExprBinary)x).op==ExprBinary.Op.AND) {
            addAND(list, ((ExprBinary)x).left);
            addAND(list, ((ExprBinary)x).right);
            return;
        }
        if (x instanceof ExprList && ((ExprList)x).op==ExprList.Op.AND) {
            for(Expr y: ((ExprList)x).args) addAND(list, y);
            return;
        }
        list.add(expr);
    }

    /** Add expr to list, in a way that flattens the disjunctions as much as possible (for better unsat core). */
    private static void addOR(TempList<Expr> list, Expr expr) {
        Expr x = expr;
        if (x instanceof ExprBinary && ((ExprBinary)x).op==ExprBinary.Op.OR) {
            addOR(list, ((ExprBinary)x).left);
            addOR(list, ((ExprBinary)x).right);
            return;
        }
        if (x instanceof ExprList && ((ExprList)x).op==ExprList.Op.OR) {
            for(Expr y: ((ExprList)x).args) addOR(list, y);
            return;
        }
        list.add(expr);
    }

    /** Generates a call to a builtin predicate */
    public static ExprList make(Pos pos, Pos closingBracket, Op op, List<Expr> args) {
    	
    	TempList<Expr> newargs = new TempList<Expr>(args.size());
    	
    	for(Expr e: args) {
    		if (op==Op.AND) 
    			addAND(newargs, e); 
    		else if (op==Op.OR) 
    			addOR(newargs, e); 
    		else 
    			newargs.add(e);
    	}
    	return new ExprList(pos, closingBracket, op, false, newargs.makeConst(), 0, emptyListOfErrors);
    }

    /** Generates the expression (arg1 and arg2 and arg3 ...) */
    public static ExprList makeAND(Expr a, Expr b) {
        TempList<Expr> list = new TempList<Expr>(2);
        list.add(a);
        list.add(b);
        return make(Pos.UNKNOWN, Pos.UNKNOWN, Op.AND, list.makeConst());
    }

    /** Generates the expression (arg1 || arg2 || arg3 ...) */
    public static ExprList makeOR(Expr a, Expr b) {
        TempList<Expr> list = new TempList<Expr>(2);
        list.add(a);
        list.add(b);
        return make(Pos.UNKNOWN, Pos.UNKNOWN, Op.OR, list.makeConst());
    }

    /** Generates the expression pred/totalOrder[arg1, args2, arg3...] */
    public static ExprList makeTOTALORDER(Pos pos, Pos closingBracket, List<Expr> args) { return make(pos, closingBracket, Op.TOTALORDER, args); }

    /** Generates the expression disj[arg1, args2, arg3...] */
    public static ExprList makeDISJOINT(Pos pos, Pos closingBracket, List<Expr> args) { return make(pos, closingBracket, Op.DISJOINT, args); }

    /** Generates the expression disj[arg1, args2, arg3...] */
    public static ExprList makeJOIN(Pos pos, Pos closingBracket, List<Expr> args) { return make(pos, closingBracket, Op.JOIN, args); }

    /** Return a new ExprList object that is the same as this one except with one additional argument. */
    public ExprList addArg(Expr x) {
        List<Expr> args = new ArrayList<Expr>(this.args);
        args.add(x);
        return make(pos, closingBracket, op, args);
    }

    //============================================================================================================//

    /** {@inheritDoc} */
    public int getDepth() {
        int max = 1;
        for(Expr x: args) { int tmp=x.getDepth(); if (max<tmp) max=tmp; }
        return 1 + max;
    }

    /** {@inheritDoc} */
    @Override final<T> T accept(VisitReturn<T> visitor) throws Err { return visitor.visit(this); }
}
